﻿using System;
using System.Collections.Generic;
using System.Text;
using DySy.Framework;
using Microsoft.Pex.Framework;

namespace DySy.Examples
{
    /// <summary>
    /// Examples from the ICSE 2008 DySy paper.
    /// </summary>
    [PexClass(typeof(ICSE08))]
    [DySyAnalysis]
    public class ICSE08
    {

        /// <summary>
        /// Example method from Figure 1 of the ICSE 2008 DySy paper.
        /// Using the Entry method below, DySy infers the desired pre-
        /// and post-condition.
        /// 
        /// Precondition inferred by DySy:
        ///   -1 < y * x
        ///   
        /// Postcondition inferred by DySy:
        ///   [(-1 < y * x && x <  y) implies (y ** 2 * x ** 2 - x ** 4)] AND
        ///   [(-1 < y * x && x >= y) implies (y ** 2 * x ** 2 - y ** 4)]
        /// </summary>
        public int testme(int x, int y)
        {
            int prod = x * y;
            if (prod < 0)
                throw new ArgumentException();
            if (x < y)
            { // swap them
                int tmp = x;
                x = y;
                y = tmp;
            }
            int sqry = y * y;
            return prod * prod - sqry * sqry;
        }


        /// <summary>
        /// Example recursive program from Section 4.2.2 of the ICSE 2008 DySy paper.
        /// DySy infers the following postcondition.
        /// 
        /// Postcondition inferred by DySy:  
        /// [(1 < i) implies (this.fac(-1 + i) * i)] AND
        /// [(i < 2) implies 1];
        /// </summary>
        public int fac(int i)
        {
            if (i <= 1)
                return 1;
            else
                return i * fac(i - 1);
        }


        /// <summary>
        /// A given execution or test case that calls the example methods.
        /// </summary>
        [PexMethod]
        public void Entry()
        {
            testme(1, 2);
            testme(2, 1);

            fac(10);
        }
    }
}
